// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

// Integer model: wrap-around
// Proof status: auto

#define X_p decimal_p
#define X_num_p decimal_num_p
#define X_val decimal_val
#define X_num_val decimal_num_val
#define X_base 10
#define sHT_X_val sHT_decimal_val
#define sHT_X_base 10
#define sHT_X_given_X_num_p sHT_decimal_given_decimal_num_p
#define sHT_X_num_p_less sHT_decimal_num_p_less
#define sHT_X_num_val_less_lt sHT_decimal_num_val_less_lt
#define sHT_X_to_u32 sHT_decimal_to_u32
#include "nat-generic.c"
